T:Type, P:(Tprop{i:l}), x:T, L:(T List).
l_all(cons(x; L); T; y.P(y))  (P(x)  l_all(L; T; y.P(y))) 

latex

Definitions	t  T, P  Q, P  Q, P  Q, x(s), l_all(L; T; x.P(x)), P  Q, prop{i:l}, x:A. B(x), True, P  Q, guard(T)
Lemmas	l member wf, cons member